Nuprl Definition : discrete-weak-precond-send-p 11,40
discrete-weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)
== ((x:Id. vartype(source(l);x) r ds(x)?Top)
== & e@source(l). (kind(e) = locl(a))  (valtype(e) r A)
== & (e:E. (kind(e) = rcv(l,tg))  (valtype(e) r T)))
== c (@source(l) discrete ds
== c  ((e':E.
== c  (((kind(e') = rcv(l,tg))
== c  (( ((kind(sender(e')) = locl(a))
== c  (( c (((P((discrete state when sender(e')))))
== c  (( c & val(e') = f((state when sender(e')),val(sender(e'))))))
== c  & e@source(l).
== c  & e':E
== c  & (e c e'
== c  & & (((kind(e') = rcv(l,tg)) c e loc sender(e') )
== c  & & ( ((loc(e') = source(l)) c (((P((discrete state after e')))))))))) 
latex

clarification:

discrete-weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)
== ((x:Id. es-vartype(es; source(l); x) r fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;source(l);e.(es-kind(es; e) = locl(a)  Knd)  (es-valtype(es; e) r A))
== & (e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  (es-valtype(es; e) r T)))
== c (es-dds(es;source(l);ds)
== c  ((e':es-E(es).
== c  (((es-kind(es; e') = rcv(l,tg)  Knd)
== c  (( ((es-kind(es; es-sender(es; e')) = locl(a)  Knd)
== c  (( c (((P(es-dstate-when(es;es-sender(es; e')))))
== c  (( c & es-val(es; e')
== c  (( c & =
== c  (( c & f(es-state-when(es;es-sender(es; e')),es-val(es; es-sender(es; e')))
== c  (( c &  T)))
== c  & alle-at(es;source(l);e.e':es-E(es)
== c  & alle-at(es;source(l);e.(es-causle(es;e;e')
== c  & alle-at(es;source(l);e.& (((es-kind(es; e') = rcv(l,tg)  Knd)
== c  & alle-at(es;source(l);e.& (c es-le(es;e;es-sender(es; e')))
== c  & alle-at(es;source(l);e.& ( ((es-loc(es; e') = source(l)  Id)
== c  & alle-at(es;source(l);e.& ( c (((P(es-dstate-after(es;e'))))))))))) 
latex

Definitionsvartype(i;x), f(x)?z, IdDeq, Top, valtype(e), @i discrete ds, x:A. B(x), P  Q, locl(a), (discrete state when e), (state when e), val(e), e@i. P(e), x:A. B(x), E, P & Q, e c e', P  Q, Knd, kind(e), rcv(l,tg), e loc e' , sender(e), A c B, s = t, Id, loc(e), source(l), A, b, f(a), (discrete state after e)
FDL editor aliasesdiscrete-weak-precond-send-p

origin